$\forall$$A$:Type, $f$:($A$$\rightarrow\mathbb{B}$), $L$:$A$ List.
\\[0ex]($\forall$$b$:$A$. ($b$ $\in$ $L$) $\Rightarrow$ $f$($b$)) $\Rightarrow$ split\_tail($L$ $\mid$ $\forall$$x$.$f$($x$)) $=$ $\langle$nil$,\,$$L$$\rangle$ $\in$ ($A$ List)$\times$($A$ List)